from cheqed.core import qparse, qterm, side
from cheqed.core.qterm import Constant, Variable,  Combination, Abstraction
from cheqed.core.sequent import Sequent

import sys
sys.setrecursionlimit(2000)

pq = qparse.parse_qtype
parser = qparse.TermParser()
pt = parser.parse

not_ = Constant('not', pq('bool->bool'))
parser.add_op(not_, 1, qparse.RIGHT)

or_ = Constant('or', pq('bool->bool->bool'))
parser.add_op(or_, 2, qparse.LEFT)

schema = Constant('schema', pq('(bool->bool)->bool'))
parser.add_binder(schema)

for_all = Constant('for_all', pq('(obj->bool)->bool'))
parser.add_binder(for_all)

exists = Constant('exists', pq('(obj->bool)->bool'))
parser.add_binder(exists)

exists_unique = Constant('exists_unique', pq('(obj->bool)->bool'))
parser.add_binder(exists_unique)

exists_class = Constant('exists_class', pq('(class->bool)->bool'))
parser.add_binder(exists_class)


# operator not:bool->bool
# operator or:bool->bool->bool
# binder for_all:(obj->bool)->bool

# derived logical operators

# operator (and)(a, b) = not (not a or not b)
and_ = Constant('and', pq('bool->bool->bool'))
parser.add_op(and_, 2, qparse.LEFT)


implies_ = Constant('implies', pq('bool->bool->bool'))
parser.add_op(implies_, 2, qparse.LEFT)

iff_ = Constant('iff', pq('bool->bool->bool'))
parser.add_op(iff_, 2, qparse.LEFT)

def define_primitives(env):
    not_ = Constant('not', pq('bool->bool'))
    env.add_op(not_, 1, qparse.RIGHT)

    or_ = Constant('or', pq('bool->bool->bool'))
    env.add_op(or_, 2, qparse.LEFT)

    for_all = Constant('for_all', pq('(obj->bool)->bool'))
    env.add_binder(for_all)

def define_derived(env):
    and_ = Constant('and', pq('bool->bool->bool'))
    env.add_op(and_, 2, qparse.LEFT)
    env.add_def('and_def',
                env.parse(r'(and) = (\x.\y.(not ((not x) or (not y))))'))

    implies_ = Constant('implies', pq('bool->bool->bool'))
    env.add_op(implies_, 2, qparse.LEFT)
    env.add_def('implies_def',
                env.parse(r'(implies) = (\x.\y.((not x) or y))'))

# set theory primitives
in_ = Constant('in', pq('obj->obj->bool'))
parser.add_op(in_, 2, qparse.LEFT)

set_of = Constant('set_of', pq('(obj->bool)->obj'))
parser.add_binder(set_of)

subset = Constant('subset', pq('obj->obj->bool'))
parser.add_op(subset, 2, qparse.LEFT)

# set theory with classes
in_class = Constant('in_class', pq('obj->class->bool'))
parser.add_op(in_class, 2, qparse.LEFT)

class_of = Constant('class_of', pq('(class->bool)->class'))
parser.add_binder(class_of)

subclass = Constant('subclass', pq('class->class->bool'))
parser.add_op(subset, 2, qparse.LEFT)

# primitive equality
equals = Constant('=', pq('?a->?a->bool'))
parser.add_op(equals, 2, qparse.LEFT)

equals_refexive = pt('a = a')
equals_symmetric = pt('(a = b) = (b = a)')
equals_transitive = pt('a = b and b = c implies a = c')

# for_all x:set, y:set . exists z:set . z = pair(x, y)
# parser.set_default_object('set')
# for_all x, y . exists z . z = pair(x, y)
# for_all x, y . exists z . z = { x, y }
# for_all phi, x . exists y . y = set_of z . z in x and phi(z)
# for_all phi, x . exists y . y = { z . z in x and phi(z) }
# for_all phi, x . exists y . y = { z in x . phi(z) }

# rules
#
# We want several things from our rule implementation. First, rules
# should be registered with a central rule list. Second, rules should
# have a fast-fail applicability test. For trivial rules this may be
# the same as applying the rule and raising an exception in case of
# failure. For rules which require significant processing time, this
# test should indicate whether there is any chance of success. Third,
# rules should advertise their parameters in a way that allows the
# interactive interface to request user input for them.

def rule(*args, **kwds):
    def annotate(fn):
        fn.extra_args = kwds
        fn.is_rule = True
        return fn
    return annotate

def match(side, string):
    def pattern(sequent):
        term = sequent[side][0]
        pattern = parser.parse(string)
        return qterm.match(pattern, term)
    
    def add_pattern(fn):
        def new_fn(*args):
            match = pattern(args[0])
            return fn(*args, **{'match':match})
        new_fn.func_name = fn.func_name
        new_fn.pattern = pattern
        return new_fn
    return add_pattern
